(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 1.
The certificate found is represented by the following graph.
Start state: 7758
Accept states: [7759, 7760]
Transitions:
7758→7759[0_1|0]
7758→7760[5_1|0]
7758→7758[1_1|0, 2_1|0, 3_1|0, 4_1|0]
7758→7761[4_1|1]
7758→7765[1_1|1]
7758→7769[4_1|1]
7758→7773[0_1|1]
7758→7777[2_1|1]
7758→7781[2_1|1]
7758→7785[2_1|1]
7758→7789[2_1|1]
7758→7793[4_1|1]
7758→7798[4_1|1]
7758→7803[4_1|1]
7758→7808[1_1|1]
7758→7813[3_1|1]
7758→7818[1_1|1]
7758→7823[0_1|1]
7758→7828[4_1|1]
7758→7833[0_1|1]
7758→7838[2_1|1]
7758→7843[2_1|1]
7758→7848[2_1|1]
7758→7853[2_1|1]
7758→7858[2_1|1]
7758→7863[2_1|1]
7758→7868[2_1|1]
7758→7873[2_1|1]
7758→7878[2_1|1]
7758→7883[2_1|1]
7758→7888[2_1|1]
7758→7893[5_1|1]
7758→7898[2_1|1]
7758→7903[4_1|1]
7758→7908[4_1|1]
7758→7913[2_1|1]
7758→7918[2_1|1]
7758→7923[0_1|1]
7758→7928[0_1|1]
7758→7933[2_1|1]
7758→7938[2_1|1]
7758→7943[0_1|1]
7761→7762[0_1|1]
7762→7763[1_1|1]
7763→7764[3_1|1]
7764→7759[2_1|1]
7764→7773[2_1|1]
7764→7823[2_1|1]
7764→7833[2_1|1]
7764→7923[2_1|1]
7764→7928[2_1|1]
7764→7943[2_1|1]
7765→7766[3_1|1]
7766→7767[0_1|1]
7767→7768[4_1|1]
7768→7759[2_1|1]
7768→7773[2_1|1]
7768→7823[2_1|1]
7768→7833[2_1|1]
7768→7923[2_1|1]
7768→7928[2_1|1]
7768→7943[2_1|1]
7769→7770[0_1|1]
7770→7771[1_1|1]
7771→7772[2_1|1]
7772→7759[3_1|1]
7772→7773[3_1|1]
7772→7823[3_1|1]
7772→7833[3_1|1]
7772→7923[3_1|1]
7772→7928[3_1|1]
7772→7943[3_1|1]
7773→7774[4_1|1]
7774→7775[1_1|1]
7775→7776[2_1|1]
7776→7759[3_1|1]
7776→7773[3_1|1]
7776→7823[3_1|1]
7776→7833[3_1|1]
7776→7923[3_1|1]
7776→7928[3_1|1]
7776→7943[3_1|1]
7777→7778[1_1|1]
7778→7779[3_1|1]
7779→7780[0_1|1]
7780→7759[4_1|1]
7780→7773[4_1|1]
7780→7823[4_1|1]
7780→7833[4_1|1]
7780→7923[4_1|1]
7780→7928[4_1|1]
7780→7943[4_1|1]
7781→7782[3_1|1]
7782→7783[0_1|1]
7783→7784[1_1|1]
7784→7759[4_1|1]
7784→7773[4_1|1]
7784→7823[4_1|1]
7784→7833[4_1|1]
7784→7923[4_1|1]
7784→7928[4_1|1]
7784→7943[4_1|1]
7785→7786[4_1|1]
7786→7787[0_1|1]
7787→7788[1_1|1]
7788→7759[4_1|1]
7788→7773[4_1|1]
7788→7823[4_1|1]
7788→7833[4_1|1]
7788→7923[4_1|1]
7788→7928[4_1|1]
7788→7943[4_1|1]
7789→7790[5_1|1]
7790→7791[0_1|1]
7791→7792[1_1|1]
7792→7759[4_1|1]
7792→7773[4_1|1]
7792→7823[4_1|1]
7792→7833[4_1|1]
7792→7923[4_1|1]
7792→7928[4_1|1]
7792→7943[4_1|1]
7793→7794[0_1|1]
7794→7795[1_1|1]
7795→7796[3_1|1]
7796→7797[0_1|1]
7797→7759[2_1|1]
7797→7773[2_1|1]
7797→7823[2_1|1]
7797→7833[2_1|1]
7797→7923[2_1|1]
7797→7928[2_1|1]
7797→7943[2_1|1]
7798→7799[4_1|1]
7799→7800[1_1|1]
7800→7801[3_1|1]
7801→7802[0_1|1]
7802→7759[2_1|1]
7802→7773[2_1|1]
7802→7823[2_1|1]
7802→7833[2_1|1]
7802→7923[2_1|1]
7802→7928[2_1|1]
7802→7943[2_1|1]
7803→7804[0_1|1]
7804→7805[4_1|1]
7805→7806[1_1|1]
7806→7807[3_1|1]
7807→7759[2_1|1]
7807→7773[2_1|1]
7807→7823[2_1|1]
7807→7833[2_1|1]
7807→7923[2_1|1]
7807→7928[2_1|1]
7807→7943[2_1|1]
7808→7809[4_1|1]
7809→7810[0_1|1]
7810→7811[3_1|1]
7811→7812[4_1|1]
7812→7759[2_1|1]
7812→7773[2_1|1]
7812→7823[2_1|1]
7812→7833[2_1|1]
7812→7923[2_1|1]
7812→7928[2_1|1]
7812→7943[2_1|1]
7813→7814[0_1|1]
7814→7815[1_1|1]
7815→7816[3_1|1]
7816→7817[4_1|1]
7817→7759[2_1|1]
7817→7773[2_1|1]
7817→7823[2_1|1]
7817→7833[2_1|1]
7817→7923[2_1|1]
7817→7928[2_1|1]
7817→7943[2_1|1]
7818→7819[4_1|1]
7819→7820[0_1|1]
7820→7821[1_1|1]
7821→7822[2_1|1]
7822→7759[3_1|1]
7822→7773[3_1|1]
7822→7823[3_1|1]
7822→7833[3_1|1]
7822→7923[3_1|1]
7822→7928[3_1|1]
7822→7943[3_1|1]
7823→7824[4_1|1]
7824→7825[1_1|1]
7825→7826[2_1|1]
7826→7827[2_1|1]
7827→7759[3_1|1]
7828→7829[0_1|1]
7829→7830[1_1|1]
7830→7831[3_1|1]
7831→7832[2_1|1]
7832→7759[3_1|1]
7832→7773[3_1|1]
7832→7823[3_1|1]
7832→7833[3_1|1]
7832→7923[3_1|1]
7832→7928[3_1|1]
7832→7943[3_1|1]
7833→7834[4_1|1]
7834→7835[1_1|1]
7835→7836[3_1|1]
7836→7837[2_1|1]
7837→7759[3_1|1]
7837→7773[3_1|1]
7837→7823[3_1|1]
7837→7833[3_1|1]
7837→7923[3_1|1]
7837→7928[3_1|1]
7837→7943[3_1|1]
7838→7839[3_1|1]
7839→7840[1_1|1]
7840→7841[3_1|1]
7841→7842[0_1|1]
7842→7759[4_1|1]
7842→7773[4_1|1]
7842→7823[4_1|1]
7842→7833[4_1|1]
7842→7923[4_1|1]
7842→7928[4_1|1]
7842→7943[4_1|1]
7843→7844[4_1|1]
7844→7845[1_1|1]
7845→7846[3_1|1]
7846→7847[0_1|1]
7847→7759[4_1|1]
7847→7773[4_1|1]
7847→7823[4_1|1]
7847→7833[4_1|1]
7847→7923[4_1|1]
7847→7928[4_1|1]
7847→7943[4_1|1]
7848→7849[3_1|1]
7849→7850[4_1|1]
7850→7851[0_1|1]
7851→7852[1_1|1]
7852→7759[4_1|1]
7852→7773[4_1|1]
7852→7823[4_1|1]
7852→7833[4_1|1]
7852→7923[4_1|1]
7852→7928[4_1|1]
7852→7943[4_1|1]
7853→7854[5_1|1]
7854→7855[4_1|1]
7855→7856[0_1|1]
7856→7857[1_1|1]
7857→7759[4_1|1]
7857→7773[4_1|1]
7857→7823[4_1|1]
7857→7833[4_1|1]
7857→7923[4_1|1]
7857→7928[4_1|1]
7857→7943[4_1|1]
7858→7859[3_1|1]
7859→7860[5_1|1]
7860→7861[0_1|1]
7861→7862[1_1|1]
7862→7759[4_1|1]
7862→7773[4_1|1]
7862→7823[4_1|1]
7862→7833[4_1|1]
7862→7923[4_1|1]
7862→7928[4_1|1]
7862→7943[4_1|1]
7863→7864[5_1|1]
7864→7865[0_1|1]
7865→7866[1_1|1]
7866→7867[1_1|1]
7867→7759[4_1|1]
7867→7773[4_1|1]
7867→7823[4_1|1]
7867→7833[4_1|1]
7867→7923[4_1|1]
7867→7928[4_1|1]
7867→7943[4_1|1]
7868→7869[5_1|1]
7869→7870[0_1|1]
7870→7871[3_1|1]
7871→7872[1_1|1]
7872→7759[4_1|1]
7872→7773[4_1|1]
7872→7823[4_1|1]
7872→7833[4_1|1]
7872→7923[4_1|1]
7872→7928[4_1|1]
7872→7943[4_1|1]
7873→7874[1_1|1]
7874→7875[3_1|1]
7875→7876[0_1|1]
7876→7877[3_1|1]
7877→7759[4_1|1]
7877→7773[4_1|1]
7877→7823[4_1|1]
7877→7833[4_1|1]
7877→7923[4_1|1]
7877→7928[4_1|1]
7877→7943[4_1|1]
7878→7879[1_1|1]
7879→7880[3_1|1]
7880→7881[0_1|1]
7881→7882[4_1|1]
7882→7759[4_1|1]
7882→7773[4_1|1]
7882→7823[4_1|1]
7882→7833[4_1|1]
7882→7923[4_1|1]
7882→7928[4_1|1]
7882→7943[4_1|1]
7883→7884[2_1|1]
7884→7885[1_1|1]
7885→7886[4_1|1]
7886→7887[4_1|1]
7887→7759[0_1|1]
7887→7773[0_1|1]
7887→7823[0_1|1]
7887→7833[0_1|1]
7887→7923[0_1|1]
7887→7928[0_1|1]
7887→7943[0_1|1]
7888→7889[2_1|1]
7889→7890[3_1|1]
7890→7891[0_1|1]
7891→7892[1_1|1]
7892→7759[4_1|1]
7892→7773[4_1|1]
7892→7823[4_1|1]
7892→7833[4_1|1]
7892→7923[4_1|1]
7892→7928[4_1|1]
7892→7943[4_1|1]
7893→7894[4_1|1]
7894→7895[4_1|1]
7895→7896[1_1|1]
7896→7897[2_1|1]
7897→7760[3_1|1]
7897→7893[3_1|1]
7898→7899[1_1|1]
7899→7900[5_1|1]
7900→7901[3_1|1]
7901→7902[4_1|1]
7902→7760[4_1|1]
7902→7893[4_1|1]
7903→7904[2_1|1]
7904→7905[0_1|1]
7905→7906[1_1|1]
7906→7907[3_1|1]
7907→7759[2_1|1]
7907→7773[2_1|1]
7907→7823[2_1|1]
7907→7833[2_1|1]
7907→7923[2_1|1]
7907→7928[2_1|1]
7907→7943[2_1|1]
7908→7909[2_1|1]
7909→7910[2_1|1]
7910→7911[0_1|1]
7911→7912[1_1|1]
7912→7759[4_1|1]
7912→7773[4_1|1]
7912→7823[4_1|1]
7912→7833[4_1|1]
7912→7923[4_1|1]
7912→7928[4_1|1]
7912→7943[4_1|1]
7913→7914[2_1|1]
7914→7915[5_1|1]
7915→7916[4_1|1]
7916→7917[4_1|1]
7917→7760[0_1|1]
7917→7893[0_1|1]
7918→7919[2_1|1]
7919→7920[3_1|1]
7920→7921[4_1|1]
7921→7922[4_1|1]
7922→7760[5_1|1]
7922→7893[5_1|1]
7923→7924[4_1|1]
7924→7925[4_1|1]
7925→7926[1_1|1]
7926→7927[3_1|1]
7927→7759[2_1|1]
7927→7773[2_1|1]
7927→7823[2_1|1]
7927→7833[2_1|1]
7927→7923[2_1|1]
7927→7928[2_1|1]
7927→7943[2_1|1]
7928→7929[4_1|1]
7929→7930[0_1|1]
7930→7931[1_1|1]
7931→7932[2_1|1]
7932→7759[3_1|1]
7932→7773[3_1|1]
7932→7823[3_1|1]
7932→7833[3_1|1]
7932→7923[3_1|1]
7932→7928[3_1|1]
7932→7943[3_1|1]
7933→7934[1_1|1]
7934→7935[3_1|1]
7935→7936[3_1|1]
7936→7937[0_1|1]
7937→7759[4_1|1]
7937→7773[4_1|1]
7937→7823[4_1|1]
7937→7833[4_1|1]
7937→7923[4_1|1]
7937→7928[4_1|1]
7937→7943[4_1|1]
7938→7939[3_1|1]
7939→7940[0_1|1]
7940→7941[4_1|1]
7941→7942[1_1|1]
7942→7759[4_1|1]
7942→7773[4_1|1]
7942→7823[4_1|1]
7942→7833[4_1|1]
7942→7923[4_1|1]
7942→7928[4_1|1]
7942→7943[4_1|1]
7943→7944[4_1|1]
7944→7945[1_1|1]
7945→7946[2_1|1]
7946→7947[2_1|1]
7947→7773[3_1|1]
7947→7823[3_1|1]
7947→7833[3_1|1]
7947→7923[3_1|1]
7947→7928[3_1|1]
7947→7943[3_1|1]